i:Id, k:Knd, l:IdLnk, ds:x:Id fp Type, da:k:Knd fp Type,
f:(tg:Id(State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List.
source(l) = i
 @i: with declarations ds:dsda:dak(v) sends f s v on link l  Dsys
 & (D:Dsys.
 & (@i: with declarations ds:dsda:dak(v) sends f s v on link l  D
 & ( D 
 & ( realizes es.
 & ( (x:Id. vartype(i;x)  ds(x)?Top)
 & ( & (e:E. loc(e) = i  Id  valtype(e)  Valtype(da;kind(e)))
 & ( & (e:E. isrcv(e)  lnk(e) = l  IdLnk  valtype(e)  Valtype(da;kind(e)))
 & ( & (e:E.
 & ( & (loc(e) = i  Id
 & ( & ( kind(e) = k  Knd
 & ( & ( (L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.
 & ( & ( ((e':E. (e'  L)  isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
 & ( & ( (& (e1, e2:E. e1 before e2  L  (e1 <loc e2))
 & ( & ( (& map(e'.<tag(e'),val(e')>;L)
 & ( & ( (& =
 & ( & ( (& tagged-list-messages(z.z when e;val(e);f)
 & ( & ( (&  (tg:IdValtype(da;rcv(l,tg))) List))) 

latex

Definitions

t  T, x:AB(x), x:A. B(x), P  Q, isrcv(k), b, <a,b>, lnk(e), isrcv(e), {T}, SQType(T), IdLnk, Prop, s ~ t, x:AB(x), left+right, valtype(e), Valtype(da;k), A & B, True, T, SqStable(P), {x:A| B(x) }, KindDeq, Type, Void, f(x)?z, Top, x.A(x), x. t(x), Id, Atom$n, vartype(i;x), x when e, State(ds), val(e), P & Q, type List, S  T, S  T, tagged-list-messages(s;v;L), E, map(f;as), (e <loc e'), x before y  l, sender(e), (x  l), P  Q, x:A. B(x), loc(e), IdDeq, es is an event system of D, ES, Dsys, D1  D2, D realizes es. P(es), , MsgA, a = b, if b t else f fi, @i: A, a:A fp B(a), source(l), @i: with declarations ds:dsda:da k(v) sends f s v on link l, kind(e), tag(e), rcv(l,tg), Knd, s = t, with declarations ds:dsda:dak(v) sends f s v on link l

Lemmas

better-sends-rule, lsrc wf, fpf wf, ifthenelse wf, eq id wf, msga wf, ma-single-sends wf, ma-empty wf, dsys wf, realizes-monotone-wrt-sub, event system wf, d-es wf, es-vartype wf, id-deq wf, top wf, es-loc wf, iff wf, l member wf, es-sender wf, l before wf, es-locl wf, map wf, es-E wf, es-lnk wf, tagged-list-messages wf, ma-state wf, es-val wf, es-when wf, Id wf, Id sq, fpf-cap wf, fpf-cap-void-subtype, Kind-deq wf, sq stable from decidable, decidable assert, es-isrcv wf, sq stable subtype rel, es-valtype wf, ma-valtype wf, Knd wf, Knd sq, rcv wf, es-tag wf, IdLnk wf, IdLnk sq, assert wf, isrcv wf, isrcv-implies, es-kind wf